Search Results

Documents authored by Abel, Andreas

Document
DOI: 10.4230/LIPIcs.TYPES.2020.1
On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction

Authors: Andreas Abel

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
Intuitionistic truth table natural deduction (ITTND) by Geuvers and Hurkens (2017), which is inherently non-confluent, has been shown strongly normalizing (SN) using continuation-passing-style translations to parallel lambda calculus by Geuvers, van der Giessen, and Hurkens (2019). We investigate the applicability of standard model-theoretic proof techniques and show (1) SN of detour reduction (β) using Girard’s reducibility candidates, and (2) SN of detour and permutation reduction (βπ) using biorthogonals. In the appendix, we adapt Tait’s method of saturated sets to β, clarifying the original proof of 2017, and extend it to βπ.
Cite as

Andreas Abel. On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{abel:LIPIcs.TYPES.2020.1,
  author =	{Abel, Andreas},
  title =	{{On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.1},
  URN =		{urn:nbn:de:0030-drops-138805},
  doi =		{10.4230/LIPIcs.TYPES.2020.1},
  annote =	{Keywords: Natural deduction, Permutative conversion, Reducibility, Strong normalization, Truth table}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2017
LIPIcs, Volume 104, TYPES'17, Complete Volume

Authors: Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi

Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)

Abstract
LIPIcs, Volume 104, TYPES'17, Complete Volume
Cite as

23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{abel_et_al:LIPIcs.TYPES.2017,
  title =	{{LIPIcs, Volume 104, TYPES'17, Complete Volume}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017},
  URN =		{urn:nbn:de:0030-drops-101671},
  doi =		{10.4230/LIPIcs.TYPES.2017},
  annote =	{Keywords: Theory of computation, Type theory, Proof theory, Program verification}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2017.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi

Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{abel_et_al:LIPIcs.TYPES.2017.0,
  author =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.0},
  URN =		{urn:nbn:de:0030-drops-100488},
  doi =		{10.4230/LIPIcs.TYPES.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.273
Well-Founded Recursion over Contextual Objects

Authors: Brigitte Pientka and Andreas Abel

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
We present a core programming language that supports writing well-founded structurally recursive functions using simultaneous pattern matching on contextual LF objects and contexts. The main technical tool is a coverage checking algorithm that also generates valid recursive calls. To establish consistency, we define a call-by-value small-step semantics and prove that every well-typed program terminates using a reducibility semantics. Based on the presented methodology we have implemented a totality checker as part of the programming and proof environment Beluga where it can be used to establish that a total Beluga program corresponds to a proof.
Cite as

Brigitte Pientka and Andreas Abel. Well-Founded Recursion over Contextual Objects. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 273-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{pientka_et_al:LIPIcs.TLCA.2015.273,
  author =	{Pientka, Brigitte and Abel, Andreas},
  title =	{{Well-Founded Recursion over Contextual Objects}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{273--287},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.273},
  URN =		{urn:nbn:de:0030-drops-51699},
  doi =		{10.4230/LIPIcs.TLCA.2015.273},
  annote =	{Keywords: Type systems, Dependent Types, Logical Frameworks}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact